FDL - Nuprl Lemma : compose-fpf-dom

Nuprl Lemma : compose-fpf-dom

A:Type, B:(A

Type), f:x:A fp

B(x), C:Type, a:(A

(C+Unit)), b:(C

A), y:C.
(y

fpf-domain(compose-fpf(a;b;f)))

(

x:A. (x

fpf-domain(f)) & isl(a(x)) & y = outl(a(x)))

Definitions t T, x(s), x. t(x), x:A. B(x), a:A fp B(a), Unit, b, fpf-domain(f), compose-fpf(a;b;f), P Q, outl(x), isl(x), Prop, A & B, (x l), P & Q, x:A. B(x), P Q, P Q, True, T, SqStable(P), if b t else f fi, , mapfilter(f;P;L)

Lemmas iff functionality wrt iff, member map filter, mapfilter wf, sq stable from decidable, decidable assert, l member wf, assert wf, isl wf, outl wf, unit wf, fpf wf